package utils.io;

import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.File;
import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;
import java.util.HashSet;
import java.util.Set;
import java.util.regex.Pattern;

import option.KBVocabulary;
import preprocessor.absorption.extended.AssertionConversion;
import preprocessor.absorption.extended.OptimizedRestrictions;

import reasoner.KBReason;

//import preprocessor.absorption.extended.ABoxConvertion;

import kb.ABox;
import kb.DescriptionLogicsKB;
import kb.TBox;

import utils.Display;
import utils.ExecTime;
//import tableaux.Completion;
import utils.parser.Parser;
import utils.exception.CoreReasoningException;
//import utils.exception.ConceptException;
import utils.exception.SyntaxParsingException;

import entities.assertion.Assertion;
import entities.axiom.Axiom;
import entities.axiom.ConceptAxiom;
import entities.axiom.RoleAxiom;
import entities.axiom.RoleInverseAxiom;

public final class KBAccess {

	private final static boolean debug = true;
	private KBAccess() {

	}
	
    public static DescriptionLogicsKB loadKB(String fileloc)
    {
        DescriptionLogicsKB kb = null;
        try {
        	System.out.println("Loading KB: "+fileloc);
            ExecTime time = ExecTime.getStarted();
            FileReader fr = new FileReader(fileloc);
            BufferedReader br = new BufferedReader(fr);
            kb = KBAccess.processKBFile(br, 
            		false, 
            		fileloc.substring(fileloc.lastIndexOf('/') + 1, fileloc.lastIndexOf('.')));
            //guarded reasoning preprocessing
            TBox tb = AssertionConversion.getConvertedTBox(kb, false);
            OptimizedRestrictions.optimize(tb);
            if(debug){
//            	System.out.println("Loading/conversion time:"+ time.getTime()/1000.0);
                System.out.printf("\nKB: %s\nAxioms:%d, CAs:%d, RAs:%d, Inds:%d \n",
                    kb.getKBName(), 
                    kb.getKBStat().getNumAx(), 
                    kb.getKBStat().getNumCA(), 
                    kb.getKBStat().getNumRA(), 
                    kb.getKBStat().getTotalInstances());
            }
            
        } catch(Exception e)  {
            e.printStackTrace();
        }
        return kb;
    }

	// ////////TBox functions
	public static TBox getTBox(String fileName) throws IOException, CoreReasoningException, SyntaxParsingException {
		return getTBox(fileName, false);
	}

	public static TBox getTBox(String fileName, boolean prime)
			throws IOException, CoreReasoningException, SyntaxParsingException {
		BufferedReader in = new BufferedReader(new FileReader(fileName));
		return getTBox(in, prime);
	}

	public static TBox getTBox(BufferedReader in) throws IOException, CoreReasoningException, SyntaxParsingException {
		return getTBox(in, false);
	}

	public static TBox getTBox(BufferedReader in, boolean prime)
			throws IOException, CoreReasoningException, SyntaxParsingException {
		// PrintStream out = new PrintStream(System.out, true, "UTF-8");

		if (in == null) {
			return null;
		}
		Set<Axiom> axs = processAxiomFile(in, prime);
		return newTBoxInstance(axs, prime);
	}

	// build a Tbox from the given axioms
	public static TBox newTBoxInstance(Set<Axiom> ax, boolean prime) 
			throws CoreReasoningException, SyntaxParsingException {
		TBox tb = new TBox();
		tb.addAxioms(ax, prime);
//		for (Axiom x : ax) {
//			if(x instanceof ConceptAxiom){
//				tb.mapAxiom(x.asConceptAxiom());
//				tb.recordOriginalAxiom(x.asConceptAxiom());
//			}else if(x instanceof RoleAxiom){
//				try {
//					tb.insertRoleAxiom(x.asRoleAxiom().asRoleInclusionAxiom(), true);
//				} catch (CoreReasoningException e) {
//					e.printStackTrace();
//				}
//			}
//
//		}
		return tb;
	}

	// return a set of axioms
	// public static HashSet<Axiom> processAxiomFile(String filename) throws
	// IOException{
	// return processAxiomFile(filename, false);
	// }

	// private static HashSet<Axiom> processAxiomFile(String filename, boolean
	// prime) throws IOException {
	// BufferedReader in = new BufferedReader(new FileReader(filename));
	// return processAxiomFile(in, prime);
	// }

	private static Set<Axiom> processAxiomFile(BufferedReader br,
			boolean prime) throws IOException {
		Set<Axiom> axs = new HashSet<Axiom>();
		try {
			String strLine;
			while ((strLine = br.readLine()) != null) {
				// no empty lines as input
				if (strLine == null || strLine.trim().equals("")
						|| strLine.startsWith(Display.COMMENTS)) {
					continue;
				}
				Axiom ax = null;
				try {
					ax = Parser.parseAxioms(
							Parser.getListOfTokensFromTokenizer(strLine), null);
				} catch (SyntaxParsingException e) {
					e.printStackTrace();
				}
				axs.add(ax);
				// if(verbose){
				// //print axioms
				// String s = ax.toString();
				// System.out.println(s +"\n--------");
				// }
				if (prime) {
					ax = ax.getPrimeCopy();
					axs.add(ax);
					// if(verbose){
					// //print axioms
					// String s = ax.toString();
					// System.out.println(s +"\n--------");
					// }
				}

			}
		} catch (IOException e) {
			e.printStackTrace();
			throw e;
		}
		return axs;
	}

	// ////////ABox Functions

	// get assertions and build an ABox from the assertions
	public static ABox newABoxInstance(HashSet<Assertion> ax) {
		ABox ab = new ABox();
		// index all assertions here
		for (Assertion a : ax) {
			ab.insertAssertions(a);
		}
		return ab;
	}

	// build an ABox from one assertion, useful for testing assertion entailment
	public static ABox newABoxInstance(Assertion a) {
		ABox ab = new ABox();
		ab.insertAssertions(a);
		return ab;
	}

	public static ABox getABox(String fileName) throws IOException {
		BufferedReader in = new BufferedReader(new FileReader(fileName));
		return getABox(in, false);
	}

	public static ABox getABox(String fileName, boolean prime)
			throws IOException {
		BufferedReader in = new BufferedReader(new FileReader(fileName));
		return getABox(in, prime);
	}

	private static ABox getABox(BufferedReader in, boolean prime)
			throws IOException {
		if (in == null) {
			return null;
		}
		HashSet<Assertion> axs = processAssertionFile(in, prime);
		ABox ab = KBAccess.newABoxInstance(axs);
		return ab;
	}

	// //return a set of assertions to be checked for entailment
	// public static HashSet<Assertion> getAssertionsToCheck(String file) throws
	// IOException{
	// BufferedReader in = new BufferedReader(new FileReader(file));
	// return getAssertionsToCheck(in);
	// }

	// private static HashSet<Assertion> getAssertionsToCheck(BufferedReader
	// br){
	// HashSet<Assertion> axs = new HashSet<Assertion>();
	// try{
	// String strLine;
	// while ((strLine = br.readLine()) != null) {
	// // no empty lines as input
	// if (strLine == null || strLine.trim().equals("")
	// ||strLine.startsWith(Display.COMMENTS)){
	// continue;
	// }else if(strLine.startsWith(Display.QUERYSYMBOL)){
	// strLine = strLine.substring(strLine.lastIndexOf(Display.QUERYSYMBOL)+1);
	// Assertion ax = null;
	// try {
	// ax = Parser.parseAssertions(Parser.getListOfTokensFromTokenizer(strLine),
	// null);
	// } catch (SyntaxParsingException e) {
	// e.printStackTrace();
	// }
	// axs.add(ax);
	// }
	// }
	// }catch(IOException e){
	// e.printStackTrace();
	// }
	// if(axs.size() < 1){
	// System.err.println("No assertions given to be checked.");
	// }
	// return axs;
	// }

	private static HashSet<Assertion> processAssertionFile(BufferedReader br,
			boolean prime) throws IOException {
		HashSet<Assertion> axs = new HashSet<Assertion>();
		try {
			String strLine;
			while ((strLine = br.readLine()) != null) {
				// no empty lines as input
				if (strLine == null || strLine.trim().equals("")
						|| strLine.startsWith(Display.COMMENTS)) {
					continue;
				}
				Assertion ax = null;
				try {
					ax = Parser.parseAssertions(
							Parser.getListOfTokensFromTokenizer(strLine), null);
				} catch (SyntaxParsingException e) {
					e.printStackTrace();
				}
				axs.add(ax);
				if (prime) {
					ax = ax.getPrimeCopy();
					axs.add(ax);
				}

			}
		} catch (IOException e) {
			e.printStackTrace();
			throw e;
		}
		return axs;
	}
	
	


	
	// both TBox and ABox are in the same file
	public static DescriptionLogicsKB processKBFile(BufferedReader br,
			boolean prime, String defaultkbname) throws IOException, SyntaxParsingException {
		KBReason.printReasonerInfo();
		TBox tb = new TBox();
		ABox ab = new ABox();
		DescriptionLogicsKB kb = DescriptionLogicsKB.newKBInstance(tb, ab,
				defaultkbname);
		Set<Axiom> axs = new HashSet<Axiom> ();
		int ca = 0, ra = 0, nax = 0;
		try {
			String strLine;
			String quoteleftd = Pattern.quote(KBVocabulary.LEFTDEL);
			while ((strLine = br.readLine()) != null) {
				if (strLine.trim().equals("")
						|| strLine.startsWith(Display.COMMENTS)) {
					continue;
				}
				if (strLine.startsWith(Display.QUERYSYMBOL)) {
					System.err
							.println("Query line or assertion check line found, ignored : "
									+ strLine);
					continue;
//				} else if (strLine.matches("^\\s*"+quoteleftd+"\\s*"+ Pattern.quote(KBVocabulary.EQAXIOM)+".+")
//						|| strLine.matches("^\\s*"+quoteleftd+"\\s*"+ Pattern.quote(KBVocabulary.IMPLIES)+".+")
//						|| strLine.matches("^\\s*"+quoteleftd+"\\s*"+ Pattern.quote(KBVocabulary.ROLEAXIOM)+".+")
//						|| strLine.matches("^\\s*"+quoteleftd+"\\s*"+ Pattern.quote(KBVocabulary.ROLE_INV)+".+")
//						|| strLine.matches("^\\s*"+quoteleftd+"\\s*"+ Pattern.quote(KBVocabulary.FEAT_DOM)+".+")
//						|| strLine.matches("^\\s*"+quoteleftd+"\\s*"+ Pattern.quote(KBVocabulary.ROLE_TRANS)+".+")
//						) {
//					Axiom ax = null;
//					try {
//						ax = Parser.parseAxioms(
//								Parser.getListOfTokensFromTokenizer(strLine),
//								kb);
//					} catch (SyntaxParsingException e) {
//						e.printStackTrace();
//					}
//					axs.add(ax);
//					nax++;
				} else if ( strLine.matches("^\\s*"+quoteleftd+"\\s*"+ Pattern.quote(KBVocabulary.CONASSERT)+".+")
						||  strLine.matches("^\\s*"+quoteleftd+"\\s*"+ Pattern.quote(KBVocabulary.ROLEASSERT)+".+")) {
					Assertion ast = null;
					try {
						ast = Parser.parseAssertions(
								Parser.getListOfTokensFromTokenizer(strLine),
								kb);
					} catch (SyntaxParsingException e) {
						e.printStackTrace();
					}
					if (strLine.contains(KBVocabulary.CONASSERT)) {
						ca++;
					} else
						ra++;
					ab.insertAssertions(ast);
					if (prime) {
						ast = ast.getPrimeCopy();
						ab.insertAssertions(ast);
					}
				} else {
					Axiom ax = null;
					try {
						ax = Parser.parseAxioms(
								Parser.getListOfTokensFromTokenizer(strLine),
								kb);
					} catch (SyntaxParsingException e) {
						e.printStackTrace();
					}
					axs.add(ax);
					nax++;
//					throw new SyntaxParsingException("Line cannot be parsed: "
//							+ strLine);
				}
			}
		//add axioms to TBox
		tb.addAxioms(axs,prime);
		} catch (IOException e) {
			e.printStackTrace();
			throw e;
		} catch (CoreReasoningException e) {
			e.printStackTrace();
		}
		kb.getKBStat().setNumAx(nax);
		kb.getKBStat().setNCA(ca);
		kb.getKBStat().setNRA(ra);
		kb.getKBStat().finalCounts();
		// ab.setNums(ca, ra);
		// if(Completion.partiallyGuardedReasoning){
		// //absorb the abox
		// try {
		// System.out.println("ABox absorbed using extended absorption...");
		// //if return a new ab, all the statistical info will be removed!
		// ab = new ABoxConvertion(ab).absorb();
		// } catch (ConceptException e) {
		// e.printStackTrace();
		// }
		//
		// }
		return kb;
	}

	public static void writeOutKBFile(String f, String s) {
		FileWriter fstream = null;
		BufferedWriter out = null;
		File file = new File(f);
		try {
			fstream = new FileWriter(file, false);
			out = new BufferedWriter(fstream);
			out.write(s);
			out.newLine();
		} catch (IOException e) {
			System.err.println("KB file cannot be generated.");
			e.printStackTrace();
		} finally {
			try {
				fstream.flush();
				// fstream.close();
				out.flush();
				out.close();
			} catch (IOException e) {
				// System.out.println("file loc: "+f);
				e.printStackTrace();
			}
		}

	}

}
